\begin{tabbing}
weak{-}precond{-}send{-}p(${\it es}$;$T$;$A$;$l$;${\it tg}$;$a$;${\it ds}$;$P$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq$r fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))\+
\\[0ex]\& alle{-}at(${\it es}$;source($l$);$e$.(es{-}kind(${\it es}$; $e$) = locl($a$) $\in$ Knd)
\\[0ex]$\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $A$))
\\[0ex]\& ($\forall$$e$:es{-}E(${\it es}$). (es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $T$)))
\\[0ex]c$\wedge$ \=((\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+\+
\\[0ex](es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ \=((es{-}kind(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) = locl($a$) $\in$ Knd)\+
\\[0ex]c$\wedge$ \=(($\uparrow$($P$(es{-}state{-}when(${\it es}$;es{-}sender(${\it es}$; ${\it e'}$)))))\+
\\[0ex]\& \=es{-}val(${\it es}$; ${\it e'}$)\+
\\[0ex]=
\\[0ex]$f$(es{-}state{-}when(${\it es}$;es{-}sender(${\it es}$; ${\it e'}$)),es{-}val(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)))
\\[0ex]$\in$ $T$)))
\-\-\-\-\\[0ex]\& alle{-}at(${\it es}$;source($l$);$e$.$\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](es{-}causle(${\it es}$;$e$;${\it e'}$)
\\[0ex]\& (\=((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)\+
\\[0ex]c$\wedge$ es{-}le(${\it es}$;$e$;es{-}sender(${\it es}$; ${\it e'}$)))
\\[0ex]$\vee$ \=((es{-}loc(${\it es}$; ${\it e'}$) = source($l$) $\in$ Id)\+
\\[0ex]c$\wedge$ \=($\neg$($\forall$$t$:$\mathbb{Q}$.\+
\\[0ex]$\uparrow$($P$(es{-}state{-}after{-}elapsed(${\it es}$;${\it e'}$;$t$))))))))))
\-\-\-\-\-\-
\end{tabbing}